<!doctype html>
<html lang="en">
  <head>
    <!-- Required meta tags -->
    <meta charset="utf-8">
    <meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">

    <!-- Bootstrap CSS -->
	<!--<link rel="stylesheet" href="css/bootstrap.min.css" >-->
	<link rel="stylesheet" href="https://leanprover-community.github.io//css/lean.css" >
	<link rel="stylesheet"
          href="https://fonts.googleapis.com/css?family=Merriweather:700">
    

	<script>
                function buildShortcutsForStructures(names) { 
                        const o = {}
                        names.forEach(name => o[name] = `\\mathbb\{${name}\}`)
                        return o
                }
		MathJax = {
			  tex: {
                                  macros: {
                                          ...buildShortcutsForStructures(["R", "Q", "Z", "N", "C"]),
                                  },
				      inlineMath: [['$', '$'], ['\\(', '\\)']]
				    },
		};
	</script>
	<script type="text/javascript" id="MathJax-script" async
		  src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-chtml.js">
	</script>

	<title>The equation compiler and using_well_founded</title>
  </head>
  <body>
  <div id="wrapper">
  <nav class="navbar navbar-expand-lg navbar-light bg-gradient-light">
    <div class="d-flex flex-grow-1">
		<a class="navbar-brand" href="https://leanprover-community.github.io/index.html">Lean Community
    </a>
    </div>

    <button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarSupportedContent" aria-controls="navbarSupportedContent" aria-expanded="false" aria-label="Toggle navigation">
      <span class="navbar-toggler-icon"></span>
    </button>
    <div class="collapse navbar-collapse flex-grow-1 text-right" id="navbarSupportedContent">
      <ul class="navbar-nav ml-auto">
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Try it!
          </a>
		  <div class="dropdown-menu " aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/lean-web-editor">Lean online</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/get_started.html">Install</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Learn
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/learn.html">Resources</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.github.io/theorem_proving_in_lean/">Theorem proving in Lean</a>
			
			
			
			<a class="dropdown-item" href="http://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/">The natural number game</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib-overview.html">Library overview</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/mathlib_docs">API documentation</a>
			
			
          </div>
        </li>
		
        <li class="nav-item dropdown">
          <a class="nav-link dropdown-toggle" href="#" id="navbarDropdown" role="button" data-toggle="dropdown" aria-haspopup="true" aria-expanded="false">
			  Community
          </a>
		  <div class="dropdown-menu  dropdown-menu-right" aria-labelledby="navbarDropdown">
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html">Meet us</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover.zulipchat.com/">Zulip chat</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/meet.html#maintainers">Maintainers</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/contribute/index.html">How to contribute</a>
			
			
			
			<a class="dropdown-item" href="https://leanprover-community.github.io/papers.html">Papers</a>
			
			
          </div>
        </li>
		
      </ul>
    </div>
  </nav>
  <div class="container-sm mt-4">
	  
<h1 id="the-equation-compiler-and-using_well_founded" class="markdown-heading">The equation compiler and using_well_founded <a class="hover-link" href="#the-equation-compiler-and-using_well_founded">#</a></h1>
<p>To define functions and proofs recursively you can use the equation compiler, if you have a well founded relation on that type</p>
<p>For example the definition of gcd on naturals uses well founded recursion</p>
<pre><code class="language-lean">def gcd : nat → nat → nat
| 0        y := y
| (succ x) y := have y % succ x &lt; succ x, from mod_lt _ $ succ_pos _,
                gcd (y % succ x) (succ x)
</code></pre>
<p>Because &lt; is a well founded relation on naturals, and because <code>y % succ x &lt; succ x</code> this recursive function is well_founded.</p>
<p>Whenever you use the equation compiler there will be a default well founded relation on the type being recursed on and the equation compiler will automatically attempt to prove the function is well founded.</p>
<p>When the equation compiler fails, there are two main causes.</p>
<ol>
<li>It has failed to prove the required inequality.</li>
<li>It is not using the correct well founded relation.</li>
</ol>
<h2 id="proving-required-inequality" class="markdown-heading">Proving required inequality <a class="hover-link" href="#proving-required-inequality">#</a></h2>
<p>If we modify the gcd example above, by removing the <code>have</code>, we get an error.</p>
<pre><code class="language-lean">def gcd : nat → nat → nat
| 0        y := y
| (succ x) y := gcd (y % succ x) (succ x)
</code></pre>
<pre><code>failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r (Σ&#x27; (a : ℕ), ℕ)
    (@psigma.has_well_founded ℕ (λ (a : ℕ), ℕ) (@has_well_founded_of_has_sizeof ℕ nat.has_sizeof)
       (λ (a : ℕ), @has_well_founded_of_has_sizeof ℕ nat.has_sizeof))
Possible solutions:
  - Use &#x27;using_well_founded&#x27; keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
  - The default decreasing tactic uses the &#x27;assumption&#x27; tactic, thus hints (aka local proofs) can be provided using &#x27;have&#x27;-expressions.
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
failed
state:
gcd : (Σ&#x27; (a : ℕ), ℕ) → ℕ,
x y : ℕ
⊢ y % succ x &lt; succ x
</code></pre>
<p>The error message has given us a goal, <code>y % succ x &lt; succ x</code>. Including a proof of this goal as part of our definition using <code>have</code> removes the error.</p>
<pre><code class="language-lean">def gcd : nat → nat → nat
| 0        y := y
| (succ x) y := have y % succ x &lt; succ x, from mod_lt _ $ succ_pos _,
                gcd (y % succ x) (succ x)
</code></pre>
<p>Note that the <code>have</code> must not be in tactics mode, i.e. inside any <code>begin</code> <code>end</code>. If you are in tactics mode, there is the option of putting the <code>have</code> statement inside the exact statement, as in the following example.</p>
<pre><code class="language-lean">def gcd : nat → nat → nat
| 0        y := y
| (succ x) y :=
begin
  exact have y % succ x &lt; succ x := mod_lt _ (succ_pos _),
  gcd (y % succ x) (succ x)
end
</code></pre>
<h2 id="order-of-arguments" class="markdown-heading">order of arguments <a class="hover-link" href="#order-of-arguments">#</a></h2>
<p>Sometimes the default relation the equation compiler uses is not the correct one. For example swapping the order of x and y in the above example causes a failure</p>
<pre><code class="language-lean">def gcd : nat → nat → nat
| y 0        := y
| y (succ x) := have y % succ x &lt; succ x, from mod_lt _ $ succ_pos _,
                gcd (succ x) (y % succ x)
</code></pre>
<p>Now the error message is asking us to prove <code>succ x &lt; y</code>. This is because by default the equation compiler tries to recurse on the first argument. More precisely, the relation that the equation compiler tries to use in this example is on the type of pairs of natural numbers <code>Σ&#x27; (a : ℕ), ℕ</code>, and it uses a lexicographical relation where the pair <code>⟨a, b⟩ ≺ ⟨c, d⟩</code> iff <code>a &lt; c ∨ (a = c ∧ b &lt; d)</code> This situation can be resolved, either by changing the order of the arguments or by specifying a <code>rel_tac</code> as decribed later in this doc.</p>
<p>Sometimes moving an argument outside of the equation compiler, can help the equation compiler prove a recursion is well_founded. For example the following proof from <code>data.nat.prime</code> fails.</p>
<pre><code class="language-lean">lemma prod_factors : ∀ (n), 0 &lt; n → list.prod (factors n) = n
| 0       h := (lt_irrefl _).elim h
| 1       h := rfl
| n@(k+2) h :=
  let m := min_fac n in have n / m &lt; n := factors_lemma,
  show list.prod (m :: factors (n / m)) = n, from
  have h₁ : 0 &lt; n / m :=
    nat.pos_of_ne_zero $ λ h,
    have n = 0 * m := (nat.div_eq_iff_eq_mul_left (min_fac_pos _) (min_fac_dvd _)).1 h,
    by rw zero_mul at this; exact (show k + 2 ≠ 0, from dec_trivial) this,
  by rw [list.prod_cons, prod_factors _ h₁, nat.mul_div_cancel&#x27; (min_fac_dvd _)]
</code></pre>
<p>But moving the <code>h</code> into a lambda after the <code>:=</code> makes it work</p>
<pre><code class="language-lean">lemma prod_factors : ∀ (n), 0 &lt; n → list.prod (factors n) = n
| 0       := λ h, (lt_irrefl _).elim h
| 1       := λ h, rfl
| n@(k+2) := λ h,
  let m := min_fac n in have n / m &lt; n := factors_lemma,
  show list.prod (m :: factors (n / m)) = n, from
  have h₁ : 0 &lt; n / m :=
    nat.pos_of_ne_zero $ λ h,
    have n = 0 * m := (nat.div_eq_iff_eq_mul_left (min_fac_pos _) (min_fac_dvd _)).1 h,
    by rw zero_mul at this; exact (show k + 2 ≠ 0, from dec_trivial) this,
  by rw [list.prod_cons, prod_factors _ h₁, nat.mul_div_cancel&#x27; (min_fac_dvd _)]
</code></pre>
<p>This is because for some reason, in the first example, the equation compiler tries to use the always false relation.</p>
<p>Conjecture : this is because the type of <code>h</code> depends on <code>n</code> and the equation compiler can only synthesize useful relations on non dependent products</p>
<h2 id="using_well_founded-rel_tac" class="markdown-heading">using_well_founded rel_tac <a class="hover-link" href="#using_well_founded-rel_tac">#</a></h2>
<p>Sometimes you need to change the well founded relation to prove that a recursion is well founded. To do this you need a <code>has_well_founded</code> instance. This is a structure with two fields, a relation and a proof that this relation is well founded. The easiest way to define a well founded relation is using a function to the natural numbers. For example on multisets the relation <code>λ s t, card s &lt; card t</code> is a well founded relation.</p>
<p>The following proof in <code>data.multiset</code> uses this relation.</p>
<pre><code class="language-lean">@[elab_as_eliminator] lemma strong_induction_on {p : multiset α → Sort*} :
  ∀ (s : multiset α), (∀ s, (∀t &lt; s, p t) → p s) → p s
| s := λ ih, ih s $ λ t h,
  have card t &lt; card s, from card_lt_of_lt h,
  strong_induction_on t ih
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf card⟩]}
</code></pre>
<p>The final line tells the equation compiler to use this relation. It is not necessary to fully understand the final line to be able to use well_founded tactics. The most important part is <code>⟨_, measure_wf card⟩</code> This is the well_founded instance. <code>measure_wf</code> is a proof that any relation generated from a function to the natural numbers, i.e. for a function <code>f : α → ℕ</code>, the relation <code>λ x y, f x &lt; f y</code>. The underscore is a placeholder for the relation, as it can be inferred from the type of the proof. Note that the well founded relation must be on a <code>psigma</code> type corresponding to the product of the types of the arguments after the vertical bar, if there are multiple arguments after the vertical bar.</p>
<p>In the gcd example the <code>psigma</code> type is <code>Σ&#x27; (a : ℕ), ℕ</code>. In order to solve the problem in the example where the order of the arguments was flipped, you could define a well founded relation on <code>Σ&#x27; (a : ℕ), ℕ</code> using the function <code>psigma.snd</code>, the function giving the second element of the pair, and then the error disappears.</p>
<pre><code class="language-lean">def gcd : nat → nat → nat
| y 0        := y
| y (succ x) := have y % succ x &lt; succ x, from mod_lt _ $ succ_pos _,
                gcd (succ x) (y % succ x)
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf psigma.snd⟩]}
</code></pre>

  </div>
</div>

  <nav class="footer navbar navbar-expand-lg navbar-light bg-light justify-content-end">
  <ul class="nav">
    <li class="nav-item">
      <a class="nav-link active" href="https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/templates/extras/well_founded_recursion.md">Suggest edits to this page on GitHub</a>
    </li>
  </ul>
</nav>

    <script src="https://code.jquery.com/jquery-3.4.1.slim.min.js" integrity="sha384-J6qa4849blE2+poT4WnyKhv5vZF5SrPo0iEjwBvKU7imGFAV0wwj1yYfoRSJoZ+n" crossorigin="anonymous"></script>
    <script src="https://leanprover-community.github.io//js/bootstrap.min.js"></script>
    
  </body>
</html>